A:Type, eq:EqDecider(A), L:(a:A fp Top List), x:A. (x  dom((L)))  (fL.x  dom(f)) 

latex

Definitions	Top, t  T, x. t(x), x:A. B(x), a:A fp B(a), type List, x:AB(x), b, (xL.P(x)), P  Q, EqDecider(T), Type, False, P  Q, P  Q, P & Q, x.A(x), , x  dom(f), [], x:A  B(x), (L), left + right, P  Q, [car / cdr], (x  l), {T}, if b then t else f fi , f  g
Lemmas	fpf-join-dom, fpf-join wf, l exists cons, fpf-join-list wf, all functionality wrt iff, iff functionality wrt iff, l exists nil, l exists wf, assert wf, fpf-dom wf, iff wf, false wf, deq wf, fpf wf, top wf